Orc is proposed as a powerful yet elegant language for distributed and concurrent programming which provides computational services such as distributed communication and data manipulation via sites. With a few concurrency primitives, programmers are able to orchestrate the invocation of sites to achieve a goal, and meanwhile, manage timeouts, priorities, and failures. To guarantee the correctness of Orc models, effective verification support is desirable.

The above illustrates the workflow of our approach. First, users can specify Orc models as well as various assertion properties via the editor. The input models of orchestration language and external services are compiled into internal representations (i.e., LTS), based on the operational semantics of Orc. On top of that Compositional Partial Order Reduction (CPOR) is applied. Linear Temporal Logic (LTL) assertions are subsequently translated into Büchi automata. Users can visualize the system behaviors via an animated simulator, or perform verification using different verifiers. If ever certain assertions or property is violated, a counterexample will be generated which can also be rendered in simulator.